EKind{i:l}  Type{i'} 

latex

Definitions	t  T, EventsWithKinds, Top, x:A. B(x), P  Q, S  T, suptype(S; T), , EOrderAxioms(E; pred?; info), P & Q
Lemmas	deq wf, top wf, unit wf, Id wf, IdLnk wf, EOrderAxioms wf, loc wf, not wf, assert wf, first wf, pred wf